The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

minus(0, x) → 0
minus(s(x), 0) → s(x)
minus(s(x), s(y)) → minus(x, y)
mod(x, 0) → 0
mod(x, s(y)) → if(lt(x, s(y)), x, s(y))
if(true, x, y) → x
if(false, x, y) → mod(minus(x, y), y)
gcd(x, 0) → x
gcd(0, s(y)) → s(y)
gcd(s(x), s(y)) → gcd(mod(s(x), s(y)), mod(s(y), s(x)))
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

minus(0, x) → 0 [1]
minus(s(x), 0) → s(x) [1]
minus(s(x), s(y)) → minus(x, y) [1]
mod(x, 0) → 0 [1]
mod(x, s(y)) → if(lt(x, s(y)), x, s(y)) [1]
if(true, x, y) → x [1]
if(false, x, y) → mod(minus(x, y), y) [1]
gcd(x, 0) → x [1]
gcd(0, s(y)) → s(y) [1]
gcd(s(x), s(y)) → gcd(mod(s(x), s(y)), mod(s(y), s(x))) [1]
lt(x, 0) → false [1]
lt(0, s(x)) → true [1]
lt(s(x), s(y)) → lt(x, y) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

minus(0, x) → 0 [1]
minus(s(x), 0) → s(x) [1]
minus(s(x), s(y)) → minus(x, y) [1]
mod(x, 0) → 0 [1]
mod(x, s(y)) → if(lt(x, s(y)), x, s(y)) [1]
if(true, x, y) → x [1]
if(false, x, y) → mod(minus(x, y), y) [1]
gcd(x, 0) → x [1]
gcd(0, s(y)) → s(y) [1]
gcd(s(x), s(y)) → gcd(mod(s(x), s(y)), mod(s(y), s(x))) [1]
lt(x, 0) → false [1]
lt(0, s(x)) → true [1]
lt(s(x), s(y)) → lt(x, y) [1]

The TRS has the following type information:

minus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s mod :: 0:s → 0:s → 0:s if :: true:false → 0:s → 0:s → 0:s lt :: 0:s → 0:s → true:false true :: true:false false :: true:false gcd :: 0:s → 0:s → 0:s

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: minus(0, x) → 0 [1] minus(s(x), 0) → s(x) [1] minus(s(x), s(y)) → minus(x, y) [1] mod(x, 0) → 0 [1] mod(x, s(y)) → if(lt(x, s(y)), x, s(y)) [1] if(true, x, y) → x [1] if(false, x, y) → mod(minus(x, y), y) [1] gcd(x, 0) → x [1] gcd(0, s(y)) → s(y) [1] gcd(s(x), s(y)) → gcd(mod(s(x), s(y)), mod(s(y), s(x))) [1] lt(x, 0) → false [1] lt(0, s(x)) → true [1] lt(s(x), s(y)) → lt(x, y) [1] The TRS has the following type information: minus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s mod :: 0:s → 0:s → 0:s if :: true:false → 0:s → 0:s → 0:s lt :: 0:s → 0:s → true:false true :: true:false false :: true:false gcd :: 0:s → 0:s → 0:s Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
true => 1
false => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

gcd(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
gcd(z, z') -{ 1 }→ gcd(mod(1 + x, 1 + y), mod(1 + y, 1 + x)) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gcd(z, z') -{ 1 }→ 1 + y :|: z' = 1 + y, y >= 0, z = 0
if(z, z', z'') -{ 1 }→ x :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 1 }→ mod(minus(x, y), y) :|: z' = x, z'' = y, x >= 0, y >= 0, z = 0
lt(z, z') -{ 1 }→ lt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
lt(z, z') -{ 1 }→ 1 :|: z' = 1 + x, x >= 0, z = 0
lt(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ 0 :|: z' = x, x >= 0, z = 0
minus(z, z') -{ 1 }→ 1 + x :|: x >= 0, z = 1 + x, z' = 0
mod(z, z') -{ 1 }→ if(lt(x, 1 + y), x, 1 + y) :|: z' = 1 + y, x >= 0, y >= 0, z = x
mod(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V9),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9),0,[mod(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9),0,[if(V, V1, V9, Out)],[V >= 0,V1 >= 0,V9 >= 0]). eq(start(V, V1, V9),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9),0,[lt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(minus(V, V1, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]). eq(minus(V, V1, Out),1,[],[Out = 1 + V3,V3 >= 0,V = 1 + V3,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V4, V5, Ret)],[Out = Ret,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(mod(V, V1, Out),1,[],[Out = 0,V6 >= 0,V = V6,V1 = 0]). eq(mod(V, V1, Out),1,[lt(V7, 1 + V8, Ret0),if(Ret0, V7, 1 + V8, Ret1)],[Out = Ret1,V1 = 1 + V8,V7 >= 0,V8 >= 0,V = V7]). eq(if(V, V1, V9, Out),1,[],[Out = V10,V1 = V10,V9 = V11,V = 1,V10 >= 0,V11 >= 0]). eq(if(V, V1, V9, Out),1,[minus(V12, V13, Ret01),mod(Ret01, V13, Ret2)],[Out = Ret2,V1 = V12,V9 = V13,V12 >= 0,V13 >= 0,V = 0]). eq(gcd(V, V1, Out),1,[],[Out = V14,V14 >= 0,V = V14,V1 = 0]). eq(gcd(V, V1, Out),1,[],[Out = 1 + V15,V1 = 1 + V15,V15 >= 0,V = 0]). eq(gcd(V, V1, Out),1,[mod(1 + V16, 1 + V17, Ret02),mod(1 + V17, 1 + V16, Ret11),gcd(Ret02, Ret11, Ret3)],[Out = Ret3,V1 = 1 + V17,V16 >= 0,V17 >= 0,V = 1 + V16]). eq(lt(V, V1, Out),1,[],[Out = 0,V18 >= 0,V = V18,V1 = 0]). eq(lt(V, V1, Out),1,[],[Out = 1,V1 = 1 + V19,V19 >= 0,V = 0]). eq(lt(V, V1, Out),1,[lt(V20, V21, Ret4)],[Out = Ret4,V1 = 1 + V21,V20 >= 0,V21 >= 0,V = 1 + V20]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(mod(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V9,Out),[V,V1,V9],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(lt(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [minus/3]
1. recursive : [lt/3]
2. recursive : [if/4, (mod)/3]
3. recursive : [gcd/3]
4. non_recursive : [start/3]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into minus/3
1. SCC is partially evaluated into lt/3
2. SCC is partially evaluated into (mod)/3
3. SCC is partially evaluated into gcd/3
4. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations minus/3
* CE 10 is refined into CE [20]
* CE 9 is refined into CE [21]
* CE 8 is refined into CE [22]


### Cost equations --> "Loop" of minus/3
* CEs [21] --> Loop 15
* CEs [22] --> Loop 16
* CEs [20] --> Loop 17

### Ranking functions of CR minus(V,V1,Out)
* RF of phase [17]: [V,V1]

#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [17]:
- RF of loop [17:1]:
V
V1


### Specialization of cost equations lt/3
* CE 19 is refined into CE [23]
* CE 17 is refined into CE [24]
* CE 18 is refined into CE [25]


### Cost equations --> "Loop" of lt/3
* CEs [24] --> Loop 18
* CEs [25] --> Loop 19
* CEs [23] --> Loop 20

### Ranking functions of CR lt(V,V1,Out)
* RF of phase [20]: [V,V1]

#### Partial ranking functions of CR lt(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1


### Specialization of cost equations (mod)/3
* CE 12 is refined into CE [26,27]
* CE 13 is refined into CE [28]
* CE 11 is refined into CE [29,30]


### Cost equations --> "Loop" of (mod)/3
* CEs [30] --> Loop 21
* CEs [29] --> Loop 22
* CEs [27] --> Loop 23
* CEs [28] --> Loop 24
* CEs [26] --> Loop 25

### Ranking functions of CR mod(V,V1,Out)
* RF of phase [21]: [V-1,V-V1]

#### Partial ranking functions of CR mod(V,V1,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V-1
V-V1


### Specialization of cost equations gcd/3
* CE 16 is refined into CE [31,32,33,34,35]
* CE 14 is refined into CE [36]
* CE 15 is refined into CE [37]


### Cost equations --> "Loop" of gcd/3
* CEs [36] --> Loop 26
* CEs [37] --> Loop 27
* CEs [35] --> Loop 28
* CEs [34] --> Loop 29
* CEs [33] --> Loop 30
* CEs [32] --> Loop 31
* CEs [31] --> Loop 32

### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [28,29]: [V+V1-4,V+2*V1-6,V+V1/2-3,2*V+V1-6,V/2+V1-3,V/2+V1/2-2,V/2+3/4*V1-11/4,2/3*V+2/3*V1-3,2/3*V+4/3*V1-13/3,3/2*V+3/4*V1-5,3/4*V+V1/2-11/4,3/4*V+3/2*V1-5,3/4*V+3/4*V1-7/2,4/3*V+2/3*V1-13/3]

#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [28,29]:
- RF of loop [28:1]:
V/2-1
V/2-V1/2 depends on loops [29:1]
- RF of loop [29:1]:
-V/2+V1/2 depends on loops [28:1]
V1/2-1


### Specialization of cost equations start/3
* CE 3 is refined into CE [38]
* CE 2 is refined into CE [39,40,41,42,43,44,45,46]
* CE 4 is refined into CE [47,48,49,50]
* CE 5 is refined into CE [51,52,53,54,55,56]
* CE 6 is refined into CE [57,58,59,60,61,62,63]
* CE 7 is refined into CE [64,65,66,67]


### Cost equations --> "Loop" of start/3
* CEs [50,54,61,66] --> Loop 33
* CEs [56,62] --> Loop 34
* CEs [63] --> Loop 35
* CEs [60] --> Loop 36
* CEs [49,53,55,59,67] --> Loop 37
* CEs [38] --> Loop 38
* CEs [43] --> Loop 39
* CEs [41] --> Loop 40
* CEs [39,48,52,58,65] --> Loop 41
* CEs [40,42,44,45,46,47,51,57,64] --> Loop 42

### Ranking functions of CR start(V,V1,V9)

#### Partial ranking functions of CR start(V,V1,V9)


Computing Bounds
=====================================

#### Cost of chains of minus(V,V1,Out):
* Chain [[17],16]: 1*it(17)+1
Such that:it(17) =< V

with precondition: [Out=0,V>=1,V1>=V]

* Chain [[17],15]: 1*it(17)+1
Such that:it(17) =< V1

with precondition: [V=Out+V1,V1>=1,V>=V1+1]

* Chain [16]: 1
with precondition: [V=0,Out=0,V1>=0]

* Chain [15]: 1
with precondition: [V1=0,V=Out,V>=1]


#### Cost of chains of lt(V,V1,Out):
* Chain [[20],19]: 1*it(20)+1
Such that:it(20) =< V

with precondition: [Out=1,V>=1,V1>=V+1]

* Chain [[20],18]: 1*it(20)+1
Such that:it(20) =< V1

with precondition: [Out=0,V1>=1,V>=V1]

* Chain [19]: 1
with precondition: [V=0,Out=1,V1>=1]

* Chain [18]: 1
with precondition: [V1=0,Out=0,V>=0]


#### Cost of chains of mod(V,V1,Out):
* Chain [[21],23]: 4*it(21)+1*s(1)+2*s(6)+3
Such that:aux(2) =< V
it(21) =< V-V1
aux(3) =< V-Out
s(1) =< Out
it(21) =< aux(2)
s(7) =< aux(2)
it(21) =< aux(3)
s(7) =< aux(3)
s(6) =< s(7)

with precondition: [Out>=1,V1>=Out+1,V>=Out+V1]

* Chain [[21],22,25]: 4*it(21)+2*s(6)+2*s(8)+7
Such that:aux(2) =< V
aux(4) =< V1
aux(5) =< V-V1
it(21) =< aux(5)
s(8) =< aux(4)
it(21) =< aux(2)
s(7) =< aux(2)
s(7) =< aux(5)
s(6) =< s(7)

with precondition: [Out=0,V1>=1,V>=2*V1]

* Chain [25]: 3
with precondition: [V=0,Out=0,V1>=1]

* Chain [24]: 1
with precondition: [V1=0,Out=0,V>=0]

* Chain [23]: 1*s(1)+3
Such that:s(1) =< V

with precondition: [V=Out,V>=1,V1>=V+1]

* Chain [22,25]: 2*s(8)+7
Such that:aux(4) =< V
s(8) =< aux(4)

with precondition: [Out=0,V=V1,V>=1]


#### Cost of chains of gcd(V,V1,Out):
* Chain [[28,29],31,27]: 7*it(28)+7*it(29)+4*s(13)+3*s(14)+2*s(16)+4*s(46)+1*s(47)+2*s(48)+2*s(49)+4*s(54)+1*s(55)+2*s(56)+12
Such that:aux(22) =< -V+V1
aux(18) =< -V+2*V1
aux(13) =< V-V1
aux(28) =< V+V1
aux(30) =< V+2*V1
aux(32) =< V+V1/2
aux(33) =< V+V1/2-Out/2
aux(42) =< V+3/2*V1-3/2*Out
aux(10) =< 2*V-V1
aux(34) =< 2*V+V1
aux(35) =< 2*V+V1-Out
aux(45) =< 2*V+2*V1-2*Out
aux(47) =< 2*V+4*V1-4*Out
aux(51) =< 3*V+2*V1-2*Out
s(10) =< 3*V+3*V1-3*Out
aux(53) =< 3*V+6*V1-6*Out
aux(49) =< 3*V+3/2*V1-3/2*Out
aux(57) =< 4*V+2*V1-2*Out
aux(16) =< -V/2+V1/2
aux(36) =< V/2
aux(37) =< V/2+V1
aux(8) =< V/2-V1/2
aux(39) =< V/2+V1/2
aux(41) =< V/2+3/4*V1
aux(44) =< 2/3*V+2/3*V1
aux(46) =< 2/3*V+4/3*V1
aux(48) =< 3/2*V+3/4*V1
aux(50) =< 3/4*V+V1/2
aux(52) =< 3/4*V+3/2*V1
aux(54) =< 3/4*V+3/4*V1
aux(56) =< 4/3*V+2/3*V1
aux(58) =< V1
aux(59) =< V1-Out
it(29) =< V1/2-Out/2
aux(6) =< Out
aux(60) =< V
aux(61) =< V+V1-Out
aux(62) =< V+2*V1-2*Out
aux(63) =< 3*V+3*V1-6*Out
s(47) =< aux(60)
s(14) =< aux(6)
s(13) =< aux(63)
s(13) =< s(10)
s(15) =< s(10)
s(15) =< aux(63)
s(16) =< s(15)
it(28) =< aux(28)
it(29) =< aux(28)
s(49) =< aux(28)
s(51) =< aux(28)
it(28) =< aux(61)
it(29) =< aux(61)
s(49) =< aux(61)
s(51) =< aux(61)
it(28) =< aux(30)
it(29) =< aux(30)
it(28) =< aux(62)
it(29) =< aux(62)
it(28) =< aux(32)
it(29) =< aux(32)
it(28) =< aux(33)
it(29) =< aux(33)
it(28) =< aux(34)
it(29) =< aux(34)
it(28) =< aux(35)
it(29) =< aux(35)
aux(15) =< aux(36)
it(28) =< aux(36)
it(28) =< aux(37)
it(29) =< aux(37)
it(28) =< aux(39)
it(29) =< aux(39)
it(28) =< aux(41)
it(29) =< aux(41)
it(28) =< aux(42)
it(29) =< aux(42)
aux(15) =< aux(60)
it(28) =< aux(60)
it(28) =< aux(44)
it(29) =< aux(44)
it(28) =< aux(45)
it(29) =< aux(45)
it(28) =< aux(46)
it(29) =< aux(46)
it(28) =< aux(47)
it(29) =< aux(47)
it(28) =< aux(48)
it(29) =< aux(48)
it(28) =< aux(49)
it(29) =< aux(49)
it(28) =< aux(50)
it(29) =< aux(50)
it(28) =< aux(51)
it(29) =< aux(51)
it(28) =< aux(52)
it(29) =< aux(52)
it(28) =< aux(53)
it(29) =< aux(53)
it(28) =< aux(54)
it(29) =< aux(54)
it(28) =< aux(63)
it(29) =< aux(63)
it(28) =< aux(56)
it(29) =< aux(56)
it(28) =< aux(57)
it(29) =< aux(57)
aux(12) =< aux(58)
s(55) =< aux(58)
aux(12) =< aux(59)
s(55) =< aux(59)
aux(7) =< aux(12)* (1/2)
aux(9) =< aux(12)*2
aux(21) =< aux(15)*2
aux(17) =< aux(15)*4
it(29) =< aux(15)+aux(16)
s(46) =< aux(12)+aux(13)
s(54) =< aux(21)+aux(22)
s(54) =< it(29)*aux(58)
s(59) =< aux(17)+aux(18)
s(59) =< it(29)*aux(58)
s(52) =< aux(9)+aux(10)
it(28) =< aux(7)+aux(8)
s(46) =< it(28)*aux(60)
s(52) =< it(28)*aux(60)
s(54) =< s(59)
s(57) =< s(59)
s(54) =< s(51)
s(57) =< s(51)
s(56) =< s(57)
s(46) =< s(52)
s(50) =< s(52)
s(46) =< s(51)
s(50) =< s(51)
s(48) =< s(50)

with precondition: [Out>=1,V1>=3*Out,V>=2*Out]

* Chain [[28,29],30,26]: 7*it(28)+7*it(29)+4*s(46)+1*s(47)+2*s(48)+2*s(49)+4*s(54)+1*s(55)+2*s(56)+3*s(60)+4*s(64)+2*s(67)+12
Such that:aux(22) =< -V+V1
aux(18) =< -V+2*V1
aux(27) =< V
aux(13) =< V-V1
aux(28) =< V+V1
aux(30) =< V+2*V1
aux(31) =< V+2*V1-Out
aux(32) =< V+V1/2
s(47) =< V-Out
aux(10) =< 2*V-V1
aux(34) =< 2*V+V1
aux(45) =< 2*V+2*V1-2*Out
aux(42) =< 2*V+3*V1-2*Out
aux(47) =< 2*V+4*V1-2*Out
aux(55) =< 3*V+3*V1-3*Out
aux(57) =< 4*V+2*V1-4*Out
aux(49) =< 6*V+3*V1-6*Out
aux(16) =< -V/2+V1/2
aux(36) =< V/2
aux(37) =< V/2+V1
aux(38) =< V/2+V1-Out/2
aux(8) =< V/2-V1/2
aux(39) =< V/2+V1/2
aux(41) =< V/2+3/4*V1
aux(43) =< V/2-Out/2
aux(44) =< 2/3*V+2/3*V1
aux(46) =< 2/3*V+4/3*V1
aux(51) =< 3/2*V+V1-3/2*Out
aux(53) =< 3/2*V+3*V1-3/2*Out
aux(48) =< 3/2*V+3/4*V1
aux(50) =< 3/4*V+V1/2
aux(52) =< 3/4*V+3/2*V1
aux(54) =< 3/4*V+3/4*V1
aux(56) =< 4/3*V+2/3*V1
aux(64) =< Out
aux(65) =< V+V1-2*Out
aux(66) =< V+V1-Out
aux(67) =< 2*V+V1-2*Out
aux(68) =< V1
it(29) =< aux(68)
s(60) =< aux(64)
s(64) =< aux(65)
s(64) =< aux(66)
s(66) =< aux(66)
s(66) =< aux(65)
s(67) =< s(66)
s(47) =< aux(27)
it(28) =< aux(28)
it(29) =< aux(28)
s(49) =< aux(28)
s(51) =< aux(28)
it(28) =< aux(65)
it(29) =< aux(65)
s(49) =< aux(65)
s(51) =< aux(65)
it(28) =< aux(30)
it(29) =< aux(30)
it(28) =< aux(31)
it(29) =< aux(31)
it(28) =< aux(32)
it(29) =< aux(32)
it(28) =< aux(67)
it(29) =< aux(67)
it(28) =< aux(34)
it(29) =< aux(34)
aux(15) =< aux(36)
it(28) =< aux(36)
it(28) =< aux(37)
it(29) =< aux(37)
it(28) =< aux(38)
it(29) =< aux(38)
it(28) =< aux(39)
it(29) =< aux(39)
it(28) =< aux(66)
it(29) =< aux(66)
it(28) =< aux(41)
it(29) =< aux(41)
it(28) =< aux(42)
it(29) =< aux(42)
aux(15) =< aux(43)
it(28) =< aux(43)
it(28) =< aux(44)
it(29) =< aux(44)
it(28) =< aux(45)
it(29) =< aux(45)
it(28) =< aux(46)
it(29) =< aux(46)
it(28) =< aux(47)
it(29) =< aux(47)
it(28) =< aux(48)
it(29) =< aux(48)
it(28) =< aux(49)
it(29) =< aux(49)
it(28) =< aux(50)
it(29) =< aux(50)
it(28) =< aux(51)
it(29) =< aux(51)
it(28) =< aux(52)
it(29) =< aux(52)
it(28) =< aux(53)
it(29) =< aux(53)
it(28) =< aux(54)
it(29) =< aux(54)
it(28) =< aux(55)
it(29) =< aux(55)
it(28) =< aux(56)
it(29) =< aux(56)
it(28) =< aux(57)
it(29) =< aux(57)
s(55) =< aux(68)
aux(7) =< aux(68)* (1/2)
aux(9) =< aux(68)*2
aux(21) =< aux(15)*2
aux(17) =< aux(15)*4
it(29) =< aux(15)+aux(16)
s(46) =< aux(68)+aux(13)
s(54) =< aux(21)+aux(22)
s(54) =< it(29)*aux(68)
s(59) =< aux(17)+aux(18)
s(59) =< it(29)*aux(68)
s(52) =< aux(9)+aux(10)
it(28) =< aux(7)+aux(8)
s(46) =< it(28)*aux(27)
s(52) =< it(28)*aux(27)
s(54) =< s(59)
s(57) =< s(59)
s(54) =< s(51)
s(57) =< s(51)
s(56) =< s(57)
s(46) =< s(52)
s(50) =< s(52)
s(46) =< s(51)
s(50) =< s(51)
s(48) =< s(50)

with precondition: [Out>=1,V>=3*Out,V1>=2*Out]

* Chain [32,26]: 4*s(69)+16
Such that:aux(69) =< V
s(69) =< aux(69)

with precondition: [Out=0,V=V1,V>=1]

* Chain [31,27]: 4*s(13)+3*s(14)+2*s(16)+12
Such that:s(10) =< V
s(12) =< V-Out
aux(6) =< Out
s(14) =< aux(6)
s(13) =< s(12)
s(13) =< s(10)
s(15) =< s(10)
s(15) =< s(12)
s(16) =< s(15)

with precondition: [V1=Out,V1>=1,V>=2*V1]

* Chain [30,26]: 3*s(60)+4*s(64)+2*s(67)+12
Such that:s(61) =< V1
s(63) =< V1-Out
aux(64) =< Out
s(60) =< aux(64)
s(64) =< s(63)
s(64) =< s(61)
s(66) =< s(61)
s(66) =< s(63)
s(67) =< s(66)

with precondition: [V=Out,V>=1,V1>=2*V]

* Chain [27]: 1
with precondition: [V=0,V1=Out,V1>=1]

* Chain [26]: 1
with precondition: [V1=0,V=Out,V>=0]


#### Cost of chains of start(V,V1,V9):
* Chain [42]: 1*s(72)+5*s(73)+8*s(77)+2*s(80)+4*s(82)+9
Such that:s(72) =< V1
aux(72) =< V1-2*V9
aux(73) =< V1-V9
aux(74) =< V9
s(77) =< aux(72)
s(82) =< aux(73)
s(73) =< aux(74)
s(77) =< aux(73)
s(79) =< aux(73)
s(79) =< aux(72)
s(80) =< s(79)

with precondition: [V=0,V1>=0]

* Chain [41]: 5
with precondition: [V1=0,V>=0]

* Chain [40]: 3
with precondition: [V=0,V9=0,V1>=1]

* Chain [39]: 3*s(90)+9
Such that:aux(75) =< V9
s(90) =< aux(75)

with precondition: [V=0,V1=2*V9,V1>=2]

* Chain [38]: 1
with precondition: [V=1,V1>=0,V9>=0]

* Chain [37]: 3*s(93)+6*s(95)+16
Such that:aux(76) =< V
aux(77) =< V1
s(93) =< aux(76)
s(95) =< aux(77)

with precondition: [V>=1,V1>=V]

* Chain [36]: 3*s(103)+4*s(104)+2*s(106)+12
Such that:s(101) =< -V+V1
s(102) =< V
s(100) =< V1
s(103) =< s(102)
s(104) =< s(101)
s(104) =< s(100)
s(105) =< s(100)
s(105) =< s(101)
s(106) =< s(105)

with precondition: [V>=1,V1>=2*V]

* Chain [35]: 7*s(140)+1*s(146)+9*s(147)+7*s(151)+2*s(152)+1*s(156)+4*s(161)+4*s(162)+2*s(166)+2*s(168)+12
Such that:s(107) =< -V+V1
s(108) =< -V+2*V1
s(142) =< V
s(109) =< V-V1
s(112) =< V+V1/2
s(115) =< 2*V-V1
s(118) =< 2*V+2*V1
s(114) =< 2*V+3*V1
s(119) =< 2*V+4*V1
s(120) =< 3*V+2*V1
s(122) =< 3*V+6*V1
s(124) =< 4*V+2*V1
s(123) =< 6*V+3*V1
s(125) =< -V/2+V1/2
s(126) =< V/2
s(127) =< V/2+V1
s(128) =< V/2-V1/2
s(129) =< V/2+V1/2
s(130) =< V/2+3/4*V1
s(131) =< 2/3*V+2/3*V1
s(132) =< 2/3*V+4/3*V1
s(133) =< 3/2*V+3/4*V1
s(134) =< 3/4*V+V1/2
s(135) =< 3/4*V+3/2*V1
s(136) =< 3/4*V+3/4*V1
s(137) =< 4/3*V+2/3*V1
aux(78) =< V+V1
aux(79) =< V+2*V1
aux(80) =< 2*V+V1
aux(81) =< 3*V+3*V1
aux(82) =< V1
s(140) =< aux(82)
s(146) =< s(142)
s(147) =< aux(81)
s(151) =< aux(78)
s(140) =< aux(78)
s(152) =< aux(78)
s(151) =< aux(79)
s(140) =< aux(79)
s(151) =< s(112)
s(140) =< s(112)
s(151) =< aux(80)
s(140) =< aux(80)
s(154) =< s(126)
s(151) =< s(126)
s(151) =< s(127)
s(140) =< s(127)
s(151) =< s(129)
s(140) =< s(129)
s(151) =< s(130)
s(140) =< s(130)
s(151) =< s(114)
s(140) =< s(114)
s(154) =< s(142)
s(151) =< s(142)
s(151) =< s(131)
s(140) =< s(131)
s(151) =< s(118)
s(140) =< s(118)
s(151) =< s(132)
s(140) =< s(132)
s(151) =< s(119)
s(140) =< s(119)
s(151) =< s(133)
s(140) =< s(133)
s(151) =< s(123)
s(140) =< s(123)
s(151) =< s(134)
s(140) =< s(134)
s(151) =< s(120)
s(140) =< s(120)
s(151) =< s(135)
s(140) =< s(135)
s(151) =< s(122)
s(140) =< s(122)
s(151) =< s(136)
s(140) =< s(136)
s(151) =< aux(81)
s(140) =< aux(81)
s(151) =< s(137)
s(140) =< s(137)
s(151) =< s(124)
s(140) =< s(124)
s(156) =< aux(82)
s(157) =< aux(82)* (1/2)
s(158) =< aux(82)*2
s(159) =< s(154)*2
s(160) =< s(154)*4
s(140) =< s(154)+s(125)
s(161) =< aux(82)+s(109)
s(162) =< s(159)+s(107)
s(162) =< s(140)*aux(82)
s(163) =< s(160)+s(108)
s(163) =< s(140)*aux(82)
s(164) =< s(158)+s(115)
s(151) =< s(157)+s(128)
s(161) =< s(151)*s(142)
s(164) =< s(151)*s(142)
s(162) =< s(163)
s(165) =< s(163)
s(162) =< aux(78)
s(165) =< aux(78)
s(166) =< s(165)
s(161) =< s(164)
s(167) =< s(164)
s(161) =< aux(78)
s(167) =< aux(78)
s(168) =< s(167)

with precondition: [V>=2,V1>=3]

* Chain [34]: 4*s(170)+7*s(172)+7*s(214)+8*s(216)+7*s(219)+1*s(223)+4*s(228)+4*s(229)+2*s(233)+2*s(235)+12
Such that:s(175) =< -V+V1
s(176) =< -V+2*V1
aux(85) =< V+V1
aux(86) =< V+2*V1
s(182) =< V+V1/2
s(184) =< 2*V-V1
aux(87) =< 2*V+V1
s(186) =< 2*V+2*V1
s(187) =< 2*V+3*V1
s(188) =< 2*V+4*V1
s(202) =< 3*V+2*V1
s(189) =< 3*V+3*V1
s(203) =< 3*V+6*V1
s(190) =< 4*V+2*V1
s(191) =< 6*V+3*V1
s(192) =< -V/2+V1/2
s(193) =< V/2
s(194) =< V/2+V1
s(196) =< V/2-V1/2
s(197) =< V/2+V1/2
s(198) =< V/2+3/4*V1
s(200) =< 2/3*V+2/3*V1
s(201) =< 2/3*V+4/3*V1
s(204) =< 3/2*V+3/4*V1
s(205) =< 3/4*V+V1/2
s(206) =< 3/4*V+3/2*V1
s(207) =< 3/4*V+3/4*V1
s(208) =< 4/3*V+2/3*V1
s(213) =< V1
aux(88) =< V
aux(89) =< V-V1
s(170) =< aux(89)
s(172) =< aux(88)
s(214) =< s(213)
s(216) =< aux(85)
s(219) =< aux(85)
s(214) =< aux(85)
s(219) =< aux(86)
s(214) =< aux(86)
s(219) =< s(182)
s(214) =< s(182)
s(219) =< aux(87)
s(214) =< aux(87)
s(222) =< s(193)
s(219) =< s(193)
s(219) =< s(194)
s(214) =< s(194)
s(219) =< s(197)
s(214) =< s(197)
s(219) =< s(198)
s(214) =< s(198)
s(219) =< s(187)
s(214) =< s(187)
s(222) =< aux(88)
s(219) =< aux(88)
s(219) =< s(200)
s(214) =< s(200)
s(219) =< s(186)
s(214) =< s(186)
s(219) =< s(201)
s(214) =< s(201)
s(219) =< s(188)
s(214) =< s(188)
s(219) =< s(204)
s(214) =< s(204)
s(219) =< s(191)
s(214) =< s(191)
s(219) =< s(205)
s(214) =< s(205)
s(219) =< s(202)
s(214) =< s(202)
s(219) =< s(206)
s(214) =< s(206)
s(219) =< s(203)
s(214) =< s(203)
s(219) =< s(207)
s(214) =< s(207)
s(219) =< s(189)
s(214) =< s(189)
s(219) =< s(208)
s(214) =< s(208)
s(219) =< s(190)
s(214) =< s(190)
s(223) =< s(213)
s(224) =< s(213)* (1/2)
s(225) =< s(213)*2
s(226) =< s(222)*2
s(227) =< s(222)*4
s(214) =< s(222)+s(192)
s(228) =< s(213)+aux(89)
s(229) =< s(226)+s(175)
s(229) =< s(214)*s(213)
s(230) =< s(227)+s(176)
s(230) =< s(214)*s(213)
s(231) =< s(225)+s(184)
s(219) =< s(224)+s(196)
s(228) =< s(219)*aux(88)
s(231) =< s(219)*aux(88)
s(229) =< s(230)
s(232) =< s(230)
s(229) =< aux(85)
s(232) =< aux(85)
s(233) =< s(232)
s(228) =< s(231)
s(234) =< s(231)
s(228) =< aux(85)
s(234) =< aux(85)
s(235) =< s(234)
s(170) =< aux(88)

with precondition: [V>=3,V1>=2]

* Chain [33]: 7*s(236)+8*s(240)+4*s(243)+12
Such that:aux(90) =< V
aux(91) =< V-V1
aux(92) =< V1
s(236) =< aux(92)
s(240) =< aux(91)
s(240) =< aux(90)
s(242) =< aux(90)
s(242) =< aux(91)
s(243) =< s(242)

with precondition: [V1>=1,V>=V1]


Closed-form bounds of start(V,V1,V9):
-------------------------------------
* Chain [42] with precondition: [V=0,V1>=0]
- Upper bound: V1+9+nat(V9)*5+nat(V1-V9)*6+nat(V1-2*V9)*8
- Complexity: n
* Chain [41] with precondition: [V1=0,V>=0]
- Upper bound: 5
- Complexity: constant
* Chain [40] with precondition: [V=0,V9=0,V1>=1]
- Upper bound: 3
- Complexity: constant
* Chain [39] with precondition: [V=0,V1=2*V9,V1>=2]
- Upper bound: 3*V9+9
- Complexity: n
* Chain [38] with precondition: [V=1,V1>=0,V9>=0]
- Upper bound: 1
- Complexity: constant
* Chain [37] with precondition: [V>=1,V1>=V]
- Upper bound: 3*V+6*V1+16
- Complexity: n
* Chain [36] with precondition: [V>=1,V1>=2*V]
- Upper bound: -V+6*V1+12
- Complexity: n
* Chain [35] with precondition: [V>=2,V1>=3]
- Upper bound: 10*V+25*V1+12+nat(-V+V1)*4+nat(-V+2*V1)*2+ (27*V+27*V1)+nat(V-V1)*4+nat(2*V-V1)*2+8*V
- Complexity: n
* Chain [34] with precondition: [V>=3,V1>=2]
- Upper bound: 22*V+31*V1+12+nat(-V+V1)*4+nat(-V+2*V1)*2+nat(V-V1)*8+nat(2*V-V1)*2+8*V
- Complexity: n
* Chain [33] with precondition: [V1>=1,V>=V1]
- Upper bound: 12*V-V1+12
- Complexity: n

### Maximum cost of start(V,V1,V9): max([max([4,nat(V9)*3+8]),V1+8+max([nat(V1-V9)*6+nat(V9)*5+nat(V1-2*V9)*8,V+V1+3+max([2*V+max([nat(-V+V1)*4,4*V1+max([4,18*V+24*V1+nat(-V+V1)*4+nat(-V+2*V1)*2+nat(2*V-V1)*2+8*V+ (V+V1+nat(V-V1)*8)])]),9*V+23*V1+nat(-V+V1)*4+nat(-V+2*V1)*2+ (27*V+27*V1)+nat(V-V1)*4+nat(2*V-V1)*2+8*V])])])+1
Asymptotic class: n
* Total analysis performed in 1269 ms.

(10) BOUNDS(1, n^1)